
% :- module.

:- use_module(library(assoc)).

:- use_module('concrete.yap').
%:- use_module('hints.yap').
:- use_module('path.yap').

initialize_constraint_list([]).

%------------------------------------ UTILITY Predicates
%---
% Get the nth item in a list
get_nth_item([I1|_Items], 0, I1).
get_nth_item([_,I1 |Items], N, _) :- 
	NewN is (N-1),
	get_nth_item([I1|Items], NewN, I1).

get_last_item([I|[]],I).
get_last_item([_|Items],_) :- get_last_item(Items,Items).

chop_list_until_nth(List,0,List).
chop_list_until_nth([_I1|Items],N,NewList) :- 
	NewN is (N-1),
	chop_list_until_nth(Items,NewN,NewList).

help_print_lv([],_Count).
help_print_lv([L1|Rest],Count) :-
	format('~w. ~w~n',[Count,L1]),
	NewCount is Count+1,
	help_print_lv(Rest,NewCount).

print_list_vertically(ListName, List):-
	format('Printing ~w------->~n',[ListName]),
	help_print_lv(List,0),
	writeln('\n').

check_tdl_append(Todo,TDL, NewTDL) :-
	((\+member(Todo, TDL)) ->
		NewTDL = [Todo | TDL]
	;
		NewTDL = TDL
	).

get_method(MC, [M | _], M) :-
	M =.. [method_body,MC,_MS1,_LC1,_ISD1,_MSD1,_CL1,_NInsList,_EC1,_E1,_TC1,_T1].
get_method(MC, [M | MT], MF) :-
	get_method(MC, MT, MF).

%-----------------------------------------------------------------------------------
% Branches / Empty
%interpret_step(S1,[IO1|IOList1],IOList1,PI,NPI,NewS1, CL, NCL, WAST) :-
%	IO1=(_O1 - I1),
%	I1 =.. [H,Arg1],
%  	isBranch(H),!,
%	concrete:instr(H,[Arg1],S1,NewS1, PI, NPI, CL, NCL, WAST).

% LookUpSwitch Check
interpret_step(S1,[IO1|IOList1],NewIOList,PI,NPI,NewS1, CL, NCL, WAST) :-
	IO1=(_O1 - I1),
	I1 =.. [lookupswitch, DO, CC, CO],
	PI =.. [path_info, _OMN, _OIC, OP],
	!,

	concrete:instr(lookupswitch, [DO, CC, CO], S1, NewS1, PI, NPI, CL, NCL, OP, WAST),
	
	NPI =..  [path_info, NMN, NIC, _NP],

	% Get the new instruction List
	b_getval(WAST, AST),
	abc_parser:getABC(method_bodies, AST, Methods),
	get_method(NMN, Methods, Meth),
	Meth =.. [method_body,_Method1,_MS1,_LC1,_ISD1,_MSD1,_CL1,NInsList,_EC1,_E1,_TC1,_T1],
	chop_list_until_nth(NInsList, NIC, NewIOList).


% No Arguments / Empty
interpret_step(S1,[IO1|IOList1],IOList1,PI,NPI,NewS1, CL, NCL, WAST) :-
	IO1=(_O1 - I1),
	I1 =.. [H],
	\+is_list(H),
	!,

	concrete:instr(I1,[],S1,NewS1, PI, NPI, CL, NCL, WAST),
	
	PI =.. [path_info, _OMN, OIC, _OP],
	NPI =..  [path_info, NMN, NIC, _NP],

	% Check if the next instruction isn't directly after the previous one
	NextOIC is (OIC+1),

	((PI=NPI) ->
		NewIOList = [IO1|IOList1]
	;

		((NextOIC = NIC) ->
			NewIOList = IOList1
		;
			% Get the new instruction List
			b_getval(WAST, AST),
    			abc_parser:getABC(method_bodies, AST, Methods),
			%nth0(NMN, Methods, Meth),
			get_method(NMN, Methods, Meth),
   			Meth =.. [method_body,_Method1,_MS1,_LC1,_ISD1,_MSD1,_CL1,NInsList,_EC1,_E1,_TC1,_T1],
			chop_list_until_nth(NInsList, NIC, NewIOList)
		)
	).

	%ASAfter =.. [abs_state,NewS1,S2,ConstraintList].
    
% 1 Argument / Empty
interpret_step(S1,[IO1|IOList1],NewIOList,PI,NPI,NewS1, CL, NCL, WAST) :-
	IO1=(_O1 - I1),
	I1 =.. [H, Arg1], !,
	
	concrete:instr(H, [Arg1], S1, NewS1, PI, NPI, CL, NCL, WAST),

	PI =.. [path_info, _OMN, OIC, _OP],
	NPI =..  [path_info, NMN, NIC, _NP],

	% Check if the next instruction isn't directly after the previous one
	NextOIC is (OIC+1),
	((NextOIC = NIC) ->
		NewIOList = IOList1
	;

		%write('Old Path Info: '), writeln(PI),
		%write('New Path Info: '), writeln(NPI),
		% Get the new instruction List
		b_getval(WAST, AST),
    		abc_parser:getABC(method_bodies, AST, Methods),

		length(Methods, MethodsCount),
		write('MC: '), writeln(MethodsCount),

		%nth0(NMN, Methods, Meth),
		get_method(NMN, Methods, Meth),

   		Meth =.. [method_body,_Method1,_MS1,_LC1,_ISD1,_MSD1,_CL1,NInsList,_EC1,_E1,_TC1,_T1],
		chop_list_until_nth(NInsList, NIC, NewIOList)
	).

%ASAfter =.. [abs_state,NewS1,S2,ConstraintList].
    
% 2 Arguments / Empty
interpret_step(S1, [IO1|IOList1], IOList1, PI, NPI, NewS1, CL, NCL, WAST) :-
	IO1=(_O1 - I1),
	I1 =.. [H, Arg1, Arg2], !,

	concrete:instr(H, [Arg1, Arg2], S1, NewS1, PI, NPI, CL, NCL, WAST).
   
% --------------------------------------------------------------------
% abstract_step(Steps, Path, CurInsList, CICount, FullInst, Abs, NewAbs, UMB, UCP)
% --------------------------------------------------------------------


% When there are no steps left, the new abstract state is complete
abstract_step(0, NewPathInfo, NewPathInfo, _IOList, _CICount, _FullInst, State, State, NCL, NCL, _WAST).

% When there are steps to take but the IO List is empty, an error has occurred
abstract_step(Steps, PathInfo, NewPathInfo, [], _CICount, _FullInst, _State, _NewState, _CL, _NCL, _WAST) :-
	writeln('ERROR: abstract_step attempting to proceed past the end of a method.'),
	break.

abstract_step(Steps, PathInfo, NewPathInfo, [IO|IOList], CICount, FullInst, State, NewState, CL, NewCL, WAST) :-
	NewSteps is (Steps - 1),

	PathInfo =.. [path_info, OMN, OIC, _OP],

	b_getval(WAST, AST),
	abc_parser:getABC(method_bodies,AST,UMethodBodies),
	get_method(OMN, UMethodBodies, RMETH),
	RMETH =.. [method_body, _Method2, _MS2, _LC2, _ISD2, _MSD2, _CL2, RInsList, _EC2, _E2, _TC2, _T2],
	nth0(OIC,RInsList,Ins),

	write('Steps: '), writeln(Steps),

	interpret_step(State, [IO|IOList], NewIOList, PathInfo, TempPathInfo, CurState, CL, NCL, WAST),
	
		CurState =.. [state,H, [EE|EEs], Trace, A],
	EE =.. [env, ScopeStack, OperandStack, RegisterFile],
	%writeln('--------------------------------------'),
	%write('IO: '), writeln(IO),
	%write('ScopeStack: '), writeln(ScopeStack),
	%write('OperandStack: '), writeln(OperandStack),
	 ((UMethodNum = 124, UInstrCount = 49) -> write('RegisterFile: '), writeln(RegisterFile); true),
	%writeln('---------------------------------------'),
	
	%	write('TPI: '), writeln(TempPathInfo),
	%	write('NPI: '), writeln(NewPathInfo),

	% If for some reason execution doesn't advance (return in the middle of the method)
	% the execution should end there
	( (PathInfo=TempPathInfo) ->
		abstract_step(0, TempPathInfo, NewPathInfo, NewIOList, (CICount+1), FullInst, CurState, NewState, NCL, NewCL, WAST)
	;
 		abstract_step(NewSteps, TempPathInfo, NewPathInfo, NewIOList, (CICount+1), FullInst, CurState, NewState, NCL, NewCL, WAST)
	).

print_todo([TD|Rest]):-
	TD = todo_item(_,Path1,Path2),
	write('[['),
	write(Path1),
	write('   '),
	write(Path2),
	write(']]'),
	print_todo(Rest).
print_todo([]).

% --------------------------------------------------------------------
% abstract_interpret( TODOLIST , ORIG_UMB, REW_UMB, ORIG_UCP, REW_UCP)
% --------------------------------------------------------------------

% When the To-Do List is empty, we are done interpreting
abstract_interpret(_Cache, []).

% When there is an item in the To-Do List, interpret it.
abstract_interpret(Cache, [TD|TDL]) :-

    writeln('\nbeginning abstract round ===============>\n'),

    b_getval(policyname, PName),

    %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
    %
    %   STEP 1: Get an arbitrary to-do item from the to-do list;;
    %   Each to-do item consists of <A,p1,p2>
    %
    %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

    TD =.. [todo_item, ABS, UPathInfo, RPathInfo],

    UPathInfo =.. [path_info, UMethodNum, UInstrCount, UP],
    RPathInfo =.. [path_info, RMethodNum, RInstrCount, RP],
    
    write('UPathInfo: '), writeln(UPathInfo),
	write('RPathInfo: '), writeln(RPathInfo),

    Key = (UPathInfo-RPathInfo),

    %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
    %
    %   Get the distance to travel down each path
    %   STEP 2: Request a hint for <A,p1,p2>.  The hint-giver responds with an abstract 
    %   state and two lengths: <B,n1,n2>.
    % 
    %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

    ( (PName = 'lus') -> 
	request_hint(ABS, UPathInfo, RPathInfo, TempRPathInfo, hint(B,ULENGTH,RLENGTH))
    ;
    	request_hint(ABS, UPathInfo, RPathInfo, hint(B,ULENGTH,RLENGTH)),
	TempRPathInfo = RPathInfo
    ),
    %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
    %
    %   STEP 3: Now abstract interpret for OLENGTH along OP and RLENGTH along 
    %   RP until getting a new abstract state C.
    %
    %   Get the appropriate methods
    %
    %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

    % Get the Global Variable Values
    b_getval(uast, UntrustedAST),
    b_getval(rast, RewrittenAST),

    % Get the Method Bodies
    abc_parser:getABC(method_bodies,UntrustedAST,UMethodBodies),
    abc_parser:getABC(method_bodies,RewrittenAST,RMethodBodies),

    get_method(UMethodNum,UMethodBodies,UMETH),
    get_method(RMethodNum,RMethodBodies,RMETH),


    UMETH =.. [method_body, _Method1, _MS1, _LC1, _ISD1, _MSD1, _CL1, UInsList, _EC1, _E1, _TC1, _T1],
    RMETH =.. [method_body, _Method2, _MS2, _LC2, _ISD2, _MSD2, _CL2, RInsList, _EC2, _E2, _TC2, _T2],
	

    % Get the appropriate instructions within the methods
    chop_list_until_nth(UInsList, UInstrCount, CurUInsList), 
    chop_list_until_nth(RInsList, RInstrCount, CurRInsList),


    ABS =.. [abs_state,UState,RState,CL0],

    CurUInsList = [TempCUI | _],
    write('Currently at position: '), writeln(UPathInfo),
    writeln(TempCUI),


    % SET A SPY POINT IF A CERTAIN INSTRUCTION IS HIT
    %((TempCUI = (7-getlex(76))) -> spy(abstract_step); true),

    ((UMethodNum = 124, UInstrCount = 49) -> writeln(UState), 	writeln(RState); true),


    abstract_step(ULENGTH, UPathInfo, NUPathInfo, CurUInsList, UInstrCount, UInsList, UState, UNewS, CL0, CL1, uast),   
    abstract_step(RLENGTH, TempRPathInfo, NRPathInfo, CurRInsList, RInstrCount, RInsList, RState, RNewS, CL1, NCL, rast),

    
    ((UMethodNum = 124, UInstrCount = 49) -> writeln(UNewS), 	writeln(RNewS) ; true),


    length(UInsList,UListLength),
    NewABS =.. [abs_state, UNewS, RNewS, NCL],

    %	((UMethodNum=835, UInstrCount=128) -> spy(add_lus_paths), break_method ; true),

    C =.. [abs_state,UNewS,RNewS,NCL],

    NUPathInfo =.. [path_info,NUMethodNum, NUInstrCount, _NUP],
    NRPathInfo =.. [path_info,NRMethodNum, NRInstrCount, _NRP],

    %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
    %
    %   STEP 4: Need to check here if C==> B
    %   	If we are in the halt case on the rewritten side, 
    %   	prove that this case isn't possible due to constraints
    %
    %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
    
	
	UNewS = state(_, _, UNewS_Trace, automaton(UNewS_State)),
	RNewS = state(_, _, RNewS_Trace, automaton(RNewS_State)),

    ( (PName = 'rbound') -> 

	((UNewS_Trace \= [], RNewS_Trace \= []) -> 
	
		UNewS_Trace = [UNewS_T | _],
		RNewS_Trace = [RNewS_T | _],

		abc_parser:getABC(constant_pool,RewrittenAST,cpoolinfo(_,_,_,_,_,_,_,TestStrings,_,_,_,_,_,TestMultinames)),
		nth(RNewS_T, TestMultinames, m_info(_, MultiNameQ)),

		((MultiNameQ = qname(_MNNamespace, TestMNName)) -> true ; true),
		((MultiNameQ = rtqname(_MNNamespace, TestMNName)) -> true ; true),
		((MultiNameQ = rtqnamel(_MNNamespace, TestMNName)) -> true ; true),
		((MultiNameQ = multiname(TestMNName, _MNNamespace)) -> true ; true),
		((MultiNameQ = multinamel(TestMNName, _MNNamespace)) -> true ; true),


		nth(TestMNName, TestStrings, string_info(_SC, _SLI, TestMethodName)),

		((UNewS_T \= RNewS_T, TestMethodName = 'exit') ->
			% If the trace variables on top don't match and the
			% rewritten trace is an exit call, we are at the halt case

			writeln('Found the halt state: checking constraints'),
			b_getval(constraintlist, CL),
			(check_constraint_list(RNewS_State) ->
				HaltFine = 1
			;
				write('Halt State failed to pass constraints at: '), writeln(NRPathInfo),
				break
			)


		; HaltFine = 0)

	; HaltFine = 0),


	( (HaltFine=1) ->
		writeln('Skip C->B for Halt State'),

		%trace,
		writeln(NRPathInfo),


		% Execute along the path in the injected code that avoids the CPV
		ModRP is (RP + 1),
		ModRLENGTH is (RLENGTH - 1),
		ModRPathInfo =.. [path_info, RMethodNum, RInstrCount, ModRP],
		%
		%spy(interpret_step),
		abstract_step(ModRLENGTH, ModRPathInfo, NModRPathInfo, CurRInsList, RInstrCount, RInsList, RState, ModRNewS, CL1, ModNCL, rast),

		ModC =.. [abs_state,UNewS,ModRNewS,ModNCL],
		CTodo =.. [todo_item,ModC,NUPathInfo,NModRPathInfo],
		NewTDL = [CTodo|TDL]
	;
		(abstract_state_implies(C, B) -> 
			writeln('satisfied.....'),

			BTodo =.. [todo_item,B,NUPathInfo,NRPathInfo],
			CTodo =.. [todo_item,C,NUPathInfo,NRPathInfo],

			( ((NUInstrCount > (UListLength - 1)) : (NUPathInfo=UPathInfo)) -> 
				TempTDL = TDL
			;		
				((get_assoc((NUPathInfo-NRPathInfo), Cache, BTodo)) ->
					TempTDL = TDL
				;
					check_tdl_append(BTodo, TDL, TempTDL)
				)
			)
		;
				      %TempTDL = TDL); 
                	 writeln('not satisfied.....'), 
		 	break
	 	)
	)
    ; true),

    ((PName = 'lus') -> 

	(abstract_state_implies(C, B) -> 
			writeln('satisfied.....'),

			BTodo =.. [todo_item,B,NUPathInfo,NRPathInfo],
			CTodo =.. [todo_item,C,NUPathInfo,NRPathInfo],

			( ((NUInstrCount > (UListLength - 1)) : (NUPathInfo=UPathInfo)) -> 
				TempTDL = TDL
			;		
				((get_assoc((NUPathInfo-NRPathInfo), Cache, BTodo)) ->
					TempTDL = TDL
				;
					check_tdl_append(BTodo, TDL, TempTDL)
				)
			)
		;
				      %TempTDL = TDL); 
                	 writeln('not satisfied.....'), 
		 	break
	 	)

    ; true),

	%((UMethodNum = 0, UInstrCount = 0) -> 
	%		writeln(TempTDL)
	%; true),

    %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
    %
    %   STEP 5: If B is not already in the cache of finished states and it's not already in 
    %   the to-do list anywhere, add <B,0,0> to the to-do list.
    %
    %   This is done every time a TODO item append is attempted
    %
    %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
    

    %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
    % 
    %   STEP 6: Add <A, next(p1,n1), next(p2,n2)> to the to-do list if next(p1,n1) and next(p2,n2) 
    %   both exist; otherwise add A to the cache of finished states.  
    %
    %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
    writeln('============================>>>>>>>>>'),

	

    length(UInsListTT, UListLength),
	CurUInsList = [HFO - FI|_],
	FI =.. [FH|_],
	%format('Current Head is ~w, UInstrCount is ~w____________________________ ~n',[FH,UInstrCount]),


    /* first check if branch instruction */

	((CurUInsList = [FirstOffset - FirstInstr|_],
	  FirstInstr =.. [H|Tail],
	  isBranch(H)) ->
		/* this is a branch instruction, so call next */
		write(H), writeln('! finding subsequent paths'),

		NewUPATHInfo =.. [path_info,UMethodNum, UInstrCount, UNewPath],
    		NewRPATHInfo =.. [path_info,RMethodNum, RInstrCount, RNewPath],

		NewKey = (NewUPATHInfo-NewRPATHInfo),
		NewTDI =.. [todo_item, ABS,NewUPATHInfo,NewRPATHInfo],

		((H=lookupswitch) ->
			((UP = 0) ->
				Tail = [DOffset, CaseCount, CaseOffsets],
				NewCaseCount is CaseCount+1,
				add_lus_paths(TempTDL, NewCaseCount, Cache, NewTDI, NewTDL)
			;
				NewTDL = TempTDL
			)
		;
			next(ABS, UPathInfo, ULENGTH, UNewPath),
    			next(ABS, TempRPathInfo, RLENGTH, RNewPath),

			((UNewPath \= -1,RNewPath \= -1) ->

				((get_assoc(NewKey, Cache, TempVal)) ->
					NewTDL = TempTDL
				;
					check_tdl_append(NewTDI, TempTDL, NewTDL)
				)

				%append(TempTDL,[todo_item(ABS,NewUPATHInfo,NewRPATHInfo)],NewTDL)
			;
				NewTDL = TempTDL
			)
		)
	;
		writeln('Not a branch, not calling next'),
		NewTDL = TempTDL),

     /* check if going past method last */
	(((NUInstrCount > (UListLength - 1)): (UInstrCount=NUInstrCount)) -> %/\ (RUInstrCount >= RCL)) ->
		writeln('NUInstrCount is greater than or = UCL'),

		% If you are past the end of a method, check to see that there is a new TD
		((NewTDL = []) ->
			% If it's empty, you are done
			writeln('Done Verification: SUCCESS!!!')
			% break

		;

			% If there's more to do, move on to the next todolist item
			writeln('reached end of this path in execution tree')

			% print_my_todo(NewTDL)
			%	format('TempTDL = ~w~n~n',[TempTDL]),
			%abstract_interpret(Cache,TempTDL)
		)
	;
	
		true),


	((get_assoc(Key, Cache, TD)) ->
		Cache = NewCache
	;
		put_assoc(Key, Cache, TD, NewCache)
	),

	

	%NewCache = [TD | Cache],

	abstract_interpret(NewCache,NewTDL).
	
add_lus_paths(TDL, 0, _, _, TDL).
add_lus_paths(OldTDL, CaseCount, Cache, todo_item(ABS,NewUPATHInfo,NewRPATHInfo), NewTDL) :-

	b_getval(policyname, PName),

	NewUPATHInfo =.. [path_info,UMethodNum, UInstrCount, _UNewPath],
    	NewRPATHInfo =.. [path_info,RMethodNum, RInstrCount, _RNewPath],

	TempUPATHInfo =.. [path_info,UMethodNum, UInstrCount, CaseCount],

	((PName='lus') ->
		% Take the CaseCount jump in the if block
		ModdedCaseCount is round(2**(1+CaseCount)),
		TempRPATHInfo =.. [path_info,RMethodNum, RInstrCount, ModdedCaseCount]
	;
		TempRPATHInfo =.. [path_info,RMethodNum, RInstrCount, CaseCount]
	),

	NewCaseCount is CaseCount - 1,

	NewKey = (TempUPATHInfo-TempRPATHInfo),

	NewTDI = todo_item(ABS,TempUPATHInfo,TempRPATHInfo),

	((get_assoc(NewKey, Cache, NewTDI)) ->
		TempTDL = OldTDL
	;
		check_tdl_append(NewTDI, OldTDL, TempTDL)
	),

	writeln('LUS PATHS: '),
	writeln(TempUPATHInfo),
	writeln(TempRPATHInfo),

	add_lus_paths(TempTDL, NewCaseCount, Cache, NewTDI, NewTDL).
   
break_method. 


init_abstract_interpret(run) :-  
%init_abstract_interpret(OEM, REM, [OUMB1|OUMBs], [RUMB1|RUMBs], OUCP, RUCP) :-
   
    % Get the Global Variable Values
    b_getval(uast, UntrustedAST),
    b_getval(rast, RewrittenAST),

    % Get the Method Bodies
    abc_parser:getABC(method_bodies, UntrustedAST, UMethodBodies),
    abc_parser:getABC(method_bodies, RewrittenAST, RMethodBodies),

    % Get the one method you want to analyze
    %nth0(3, UMethodBodies, UCheckMethod),
    %nth0(3, RMethodBodies, RCheckMethod),
    %fill_initial_todo([UCheckMethod], [RCheckMethod], 3, 3, [], NewTDL),

    fill_initial_todo(UMethodBodies, RMethodBodies, 0, 0, [], NewTDL),

    empty_assoc(Cache),
    abstract_interpret(Cache, NewTDL).
    
fill_initial_todo([], [], _, _, TDL, TDL).

fill_initial_todo([UMB | UMBs], [RMB | RMBs], UC, RC, TDL, NewTDL) :-

    % Construct Initial Abstract state
    concrete:initialize_start_state(S1_0),
    concrete:initialize_start_state(S2_0),

    S1_0 =.. [state, H1, [EE1], [], A1],
    S2_0 =.. [state, H2, [EE2], [], A2],

    EE1 =.. [env, SS1, OS1, _RF1],
    EE2 =.. [env, SS2, OS2, _RF2],

    UMB =.. [method_body,Method1,_MS1,LC1,_ISD1,_MSD1,_CL1,_C1,_EC1,_E1,_TC1,_T1],
    RMB =.. [method_body,Method2,_MS2,LC2,_ISD2,_MSD2,_CL2,_C2,_EC2,_E2,_TC2,_T2],

    length(NewRF1,LC1),
    length(NewRF2,LC2),
    concrete:top_list(NewRF1),
    concrete:top_list(NewRF2),

    NewEE1 =.. [env,SS1,OS1,NewRF1],
    NewEE2 =.. [env,SS2,OS2,NewRF2],
    NewS1_0 =.. [state, H1, [NewEE1], [], A1],
    NewS2_0 =.. [state, H2, [NewEE2], [], A2],

    initialize_constraint_list(ConstraintList_0),
    AS_0 =.. [abs_state,NewS1_0,NewS2_0,ConstraintList_0],

    OPathInfo =.. [path_info,Method1,0,0],
    RPathInfo =.. [path_info,Method2,0,0],

    NTD =.. [todo_item,AS_0,OPathInfo,RPathInfo],

    NewUC is (UC+1),
    NewRC is (RC+1),

    fill_initial_todo(UMBs, RMBs, NewUC, NewRC, [NTD | TDL], NewTDL).

print_my_todo([]).
print_my_todo([TD|TDL]) :-
	writeln(TD),
	print_my_todo(TDL).

% Helper function, determines if the instruction is a branching jump instruction
isBranch(ifeq).
isBranch(iffalse).
isBranch(ifge).
isBranch(ifgt).
isBranch(ifle).
isBranch(iflt).
isBranch(ifnge).
isBranch(ifngt).
isBranch(ifnle).
isBranch(ifnlt).
isBranch(ifne).
isBranch(ifstricteq).
isBranch(ifstrictne).
isBranch(iftrue).
isBranch(lookupswitch).




